<html>
<head><meta charset="utf-8"><title>coinduction · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html">coinduction</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="228487921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/228487921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#228487921">(Mar 02 2021 at 21:20)</a>:</h4>
<p>So <span class="user-mention" data-user-id="365822">@FireFighterDuck</span> I was re-reading the issue and I saw that I <a href="https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016">left this comment</a> about an alternative approach for handling coinduction</p>



<a name="228487969"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/228487969" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#228487969">(Mar 02 2021 at 21:20)</a>:</h4>
<p>I'm curious if you considered and rejected that</p>



<a name="228488077"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/228488077" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#228488077">(Mar 02 2021 at 21:21)</a>:</h4>
<p>My approach is more or less based on this comment.</p>



<a name="228488110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/228488110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#228488110">(Mar 02 2021 at 21:21)</a>:</h4>
<p>ok</p>



<a name="229620339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/229620339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#229620339">(Mar 10 2021 at 08:31)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/meeting.202021-03-09/near/229554609">said</a>:</p>
<blockquote>
<p>basically there is already a mechanism for "temporary cached results"</p>
</blockquote>
<p>As a small followup from yesterdays meeting, I would like to get some clarity on this. Did you mean the mechanism for delaying results inside an inductive cycle by leaving them on the graph? Or did you mean the cache in <code>RecursiveContext</code> (which as far as I understand is not really temporary)?</p>



<a name="230009213"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230009213" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230009213">(Mar 12 2021 at 10:51)</a>:</h4>
<p><span class="user-mention" data-user-id="365822">@FireFighterDuck</span> I meant the mechanism for delaying results inside of inductive cycles, I think</p>



<a name="230011194"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230011194" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230011194">(Mar 12 2021 at 11:07)</a>:</h4>
<p>Yeah, that was essentially what the closed PR was about. I had some intuition because of which I didn't follow this approach any further but I'd need to think about it again.</p>



<a name="230044899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230044899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230044899">(Mar 12 2021 at 15:13)</a>:</h4>
<p>I'm going to give this a bit of thought :)</p>



<a name="230094335"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230094335" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230094335">(Mar 12 2021 at 20:41)</a>:</h4>
<p>today ran away from from me (sigh)</p>



<a name="230094349"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230094349" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230094349">(Mar 12 2021 at 20:41)</a>:</h4>
<p>but I'm opening up the PR now :)</p>



<a name="230095472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230095472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230095472">(Mar 12 2021 at 20:51)</a>:</h4>
<p>I'm also reading <a href="https://github.com/rust-lang/chalk/issues/683">chalk#683</a></p>



<a name="230095668"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230095668" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230095668">(Mar 12 2021 at 20:52)</a>:</h4>
<p><span class="user-mention" data-user-id="365822">@FireFighterDuck</span> what motivated <a href="https://github.com/rust-lang/rust/issues/690">#690</a> over <a href="https://github.com/rust-lang/rust/issues/683">#683</a>? were there specific tests or things that weren't working? I can't quite follow from your comments</p>



<a name="230098135"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230098135" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230098135">(Mar 12 2021 at 21:10)</a>:</h4>
<p>It wasn't really a test or anything just unexpected behaviour. <a href="https://github.com/rust-lang/chalk/issues/683">chalk#683</a> uses the same delaying method for coinductive cycles as for inductive cycles, i.e. it leaves the nodes in the search graph. Unfortunately, the existence of nodes in the graph is also used to recognize inductive cycle start. Thus, delayed results were interpreted as part of an inductive cycle. This still worked for all tests but it seemed too "hacky" to me to work for more complicated cases.</p>
<p>tl;dr I simply didn't think enough about it. The other approach seemed simpler to understand and implement correctly.</p>



<a name="230103152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230103152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230103152">(Mar 12 2021 at 21:47)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span>  Small update: The simple usage of the minimums (like in <a href="https://github.com/rust-lang/chalk/issues/683">chalk#683</a>) does not work for nested coinductive cycles like in the <code>coinductive_unsound_inter_cycle_dependency</code> test I added in <a href="https://github.com/rust-lang/chalk/issues/690">chalk#690</a> . There, the false positives still occur. I'm not sure, how likely and thus relevant this is in real world applications though.</p>



<a name="230160888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/230160888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#230160888">(Mar 13 2021 at 12:51)</a>:</h4>
<p><span class="user-mention" data-user-id="365822">@FireFighterDuck</span> that's helpful, thanks, let me dig into that example!</p>



<a name="231800528"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231800528" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231800528">(Mar 25 2021 at 13:33)</a>:</h4>
<p>What I wanted to do when I get back is to walk through some examples (in particular the one <span class="user-mention" data-user-id="365822">@FireFighterDuck</span> raised) in detail with the new PR</p>



<a name="231804090"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804090" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804090">(Mar 25 2021 at 13:55)</a>:</h4>
<p>ok, back</p>



<a name="231804459"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804459" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804459">(Mar 25 2021 at 13:57)</a>:</h4>
<p>howdy</p>



<a name="231804564"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804564" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804564">(Mar 25 2021 at 13:58)</a>:</h4>
<p>maybe we can start with</p>



<a name="231804573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804573">(Mar 25 2021 at 13:58)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1orC2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C3</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231804645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804645">(Mar 25 2021 at 13:58)</a>:</h4>
<p>actually let's just do</p>



<a name="231804647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804647">(Mar 25 2021 at 13:58)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="nf">coinductive_unsound1</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">test</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">test</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="n">program</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="n">program</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1orC2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1orC2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C3</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C3</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231804707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804707">(Mar 25 2021 at 13:59)</a>:</h4>
<p>ugh</p>



<a name="231804737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804737">(Mar 25 2021 at 13:59)</a>:</h4>
<p>There are just the same examples we worked on for the SLG solver?</p>



<a name="231804785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804785">(Mar 25 2021 at 13:59)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="nf">coinductive_unsound1</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">test</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="n">program</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1orC2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C3</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>

<span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">X</span>: <span class="nc">C1orC2</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="s">"No possible solution"</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231804793"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804793" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804793">(Mar 25 2021 at 13:59)</a>:</h4>
<p>this is the basic example</p>



<a name="231804878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804878">(Mar 25 2021 at 14:00)</a>:</h4>
<p>just to refresh some memory, bring back Ye Good Olde Days</p>



<a name="231804993"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231804993" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231804993">(Mar 25 2021 at 14:00)</a>:</h4>
<div class="message_inline_image"><a href="https://media.giphy.com/media/3o6MbmL5HRG8KCL3by/source.gif"><img src="https://media.giphy.com/media/3o6MbmL5HRG8KCL3by/source.gif"></a></div>



<a name="231805080"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805080" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805080">(Mar 25 2021 at 14:00)</a>:</h4>
<p>brb, one sec</p>



<a name="231805157"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805157" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805157">(Mar 25 2021 at 14:01)</a>:</h4>
<p>so in the recursive solver...</p>



<a name="231805311"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805311" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805311">(Mar 25 2021 at 14:02)</a>:</h4>
<p>we start proving <code>C1orC2</code> and we have two routes to explore</p>



<a name="231805370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805370">(Mar 25 2021 at 14:02)</a>:</h4>
<p>we go down the <code>T: C1</code> (let's say) and that will take us to <code>T: C2</code></p>



<a name="231805379"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805379" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805379">(Mar 25 2021 at 14:02)</a>:</h4>
<p>let me make a tree</p>



<a name="231805569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805569">(Mar 25 2021 at 14:03)</a>:</h4>
<ul>
<li><code>!X: C1orC2</code><br>
    * <code>X: C1orC1 if X: C1</code><br>
        * <code>X: C1 if X: C2, X: C3</code><br>
            * <code>X: C2 if X: C1</code><br>
                * <code>X: C1</code> -- inductive cycle</li>
</ul>



<a name="231805583"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805583" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805583">(Mar 25 2021 at 14:03)</a>:</h4>
<p>ugh</p>



<a name="231805591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805591">(Mar 25 2021 at 14:03)</a>:</h4>
<p>I'm making a hackmd</p>



<a name="231805715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805715">(Mar 25 2021 at 14:04)</a>:</h4>
<p>back</p>



<a name="231805718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231805718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231805718">(Mar 25 2021 at 14:04)</a>:</h4>
<p><a href="https://hackmd.io/2nm3xPJ1TTGc2r4iiWi4Lg">https://hackmd.io/2nm3xPJ1TTGc2r4iiWi4Lg</a></p>



<a name="231806139"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231806139" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231806139">(Mar 25 2021 at 14:06)</a>:</h4>
<p>So you're writing the goals we have to solve?</p>



<a name="231806219"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231806219" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231806219">(Mar 25 2021 at 14:07)</a>:</h4>
<p>yeah that's kind of the path the recursive solver takes</p>



<a name="231806507"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231806507" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231806507">(Mar 25 2021 at 14:08)</a>:</h4>
<p>I'm starting to remember some things</p>



<a name="231806574"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231806574" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231806574">(Mar 25 2021 at 14:09)</a>:</h4>
<p>so when it hits the cycle</p>



<a name="231806935"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231806935" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231806935">(Mar 25 2021 at 14:11)</a>:</h4>
<p>ugh silly vscode extension</p>



<a name="231807023"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807023" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807023">(Mar 25 2021 at 14:11)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L134-L139">https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L134-L139</a></p>



<a name="231807103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807103">(Mar 25 2021 at 14:12)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/coinduction/near/231806935">said</a>:</p>
<blockquote>
<p>ugh silly vscode extension</p>
</blockquote>
<p>(you have to have a remote named <code>origin</code> for it to do the right thing)</p>



<a name="231807174"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807174" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807174">(Mar 25 2021 at 14:12)</a>:</h4>
<p><span aria-label="upside down" class="emoji emoji-1f643" role="img" title="upside down">:upside_down:</span></p>



<a name="231807295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807295">(Mar 25 2021 at 14:13)</a>:</h4>
<p>So, is there are reason we can't employ a similiar "delayed subgoal" approach in the recursive solver?</p>



<a name="231807338"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807338" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807338">(Mar 25 2021 at 14:13)</a>:</h4>
<p>I don't want to do that</p>



<a name="231807379"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807379" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807379">(Mar 25 2021 at 14:13)</a>:</h4>
<p>I think we plausibly <em>could</em> but the recursive solver has other options :)</p>



<a name="231807411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807411">(Mar 25 2021 at 14:13)</a>:</h4>
<p>anyway let's walk through because I have to bring it back</p>



<a name="231807429"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807429" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807429">(Mar 25 2021 at 14:13)</a>:</h4>
<p>sorry, I'm being slow</p>



<a name="231807460"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807460" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807460">(Mar 25 2021 at 14:13)</a>:</h4>
<p>so we invoke <code>solve_iteration</code></p>



<a name="231807535"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807535" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807535">(Mar 25 2021 at 14:14)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/solve.rs#L38-L42">https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/solve.rs#L38-L42</a></p>



<a name="231807656"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807656" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807656">(Mar 25 2021 at 14:14)</a>:</h4>
<p>which will invoke <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/solve.rs#L121-L125"><code>solve_from_clauses</code></a></p>



<a name="231807817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807817">(Mar 25 2021 at 14:15)</a>:</h4>
<p>this creates a fulfillment context</p>



<a name="231807902"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807902" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807902">(Mar 25 2021 at 14:16)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/solve.rs#L165-L166">here</a></p>



<a name="231807988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231807988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231807988">(Mar 25 2021 at 14:16)</a>:</h4>
<p>and invokes <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/fulfill.rs#L518-L519"><code>solve()</code></a></p>



<a name="231808188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808188">(Mar 25 2021 at 14:17)</a>:</h4>
<p>which invokes <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/fulfill.rs#L437-L438"><code>fulfill()</code></a></p>



<a name="231808243"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808243" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808243">(Mar 25 2021 at 14:17)</a>:</h4>
<p>which invokes <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/fulfill.rs#L462-L466"><code>prove()</code></a></p>



<a name="231808301"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808301" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808301">(Mar 25 2021 at 14:17)</a>:</h4>
<p>which <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/fulfill.rs#L357-L358">calls <code>self.solver.solve_goal()</code></a></p>



<a name="231808421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808421">(Mar 25 2021 at 14:18)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L211-L215">defined here</a></p>



<a name="231808505"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808505" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808505">(Mar 25 2021 at 14:18)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L222-L226">which detects the cycle</a></p>



<a name="231808553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808553">(Mar 25 2021 at 14:19)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L231-L241">and detects that it is coinductive here</a></p>



<a name="231808620"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808620" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808620">(Mar 25 2021 at 14:19)</a>:</h4>
<p>importantly, we don't update the <code>minimums</code> at all</p>



<a name="231808657"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808657" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808657">(Mar 25 2021 at 14:19)</a>:</h4>
<p>the <code>minimums</code> is used to track what part of the stack this result depends on</p>



<a name="231808679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808679">(Mar 25 2021 at 14:19)</a>:</h4>
<p>(and how)</p>



<a name="231808697"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808697" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808697">(Mar 25 2021 at 14:20)</a>:</h4>
<p>we don't even flag this as a cycle</p>



<a name="231808754"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231808754" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231808754">(Mar 25 2021 at 14:20)</a>:</h4>
<p>ok</p>



<a name="231809001"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231809001" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231809001">(Mar 25 2021 at 14:21)</a>:</h4>
<p>this affects caching because</p>



<a name="231809645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231809645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231809645">(Mar 25 2021 at 14:24)</a>:</h4>
<p>if we pop back up to <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L134-L139"><code>solve_new_subgoal</code></a>, where this whole thing started</p>



<a name="231809718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231809718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231809718">(Mar 25 2021 at 14:24)</a>:</h4>
<p>actually no, higher than that</p>



<a name="231809734"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231809734" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231809734">(Mar 25 2021 at 14:25)</a>:</h4>
<p>well, solve-new-subgoal basically loops</p>



<a name="231809821"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231809821" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231809821">(Mar 25 2021 at 14:25)</a>:</h4>
<p>we gotta go <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L211-L215"><code>solve_goal</code></a></p>



<a name="231810017"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810017" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810017">(Mar 25 2021 at 14:26)</a>:</h4>
<p>once we've reached the fixed point, basically, we cache but only if the <a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L272-L288">"minimum" is <code>&gt;= dfn</code>"</a> -- meaning that this did not depend on anything outside of its subtree</p>



<a name="231810072"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810072" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810072">(Mar 25 2021 at 14:26)</a>:</h4>
<p>in this case, we have not altered minimum, so we don't realize that it depends on something outside of its subtree</p>



<a name="231810110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810110">(Mar 25 2021 at 14:26)</a>:</h4>
<p>but of course it does -- it depends on itself</p>



<a name="231810205"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810205" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810205">(Mar 25 2021 at 14:27)</a>:</h4>
<p>(not sure if anybody is even listening here lol but it seems useful to just dump stream of consciousness here...)</p>



<a name="231810368"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810368" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810368">(Mar 25 2021 at 14:28)</a>:</h4>
<p>I am</p>



<a name="231810457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810457">(Mar 25 2021 at 14:28)</a>:</h4>
<p>so, one thing we could do is to alter the minimums</p>



<a name="231810490"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810490" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810490">(Mar 25 2021 at 14:29)</a>:</h4>
<p>You're doing what I've done with like the binder refactor stuff</p>



<a name="231810507"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810507" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810507">(Mar 25 2021 at 14:29)</a>:</h4>
<p>Its helpful</p>



<a name="231810551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810551">(Mar 25 2021 at 14:29)</a>:</h4>
<p>(ps cc <span class="user-mention" data-user-id="116266">@Santiago Pastorino</span> who has been asking me to follow up with braindumps from time to time :)</p>



<a name="231810794"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810794" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810794">(Mar 25 2021 at 14:30)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/lib.rs#L15-L20"><code>Minimums</code></a> is sort of a misnomer</p>



<a name="231810817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810817">(Mar 25 2021 at 14:30)</a>:</h4>
<p>that we don't properly handle negative subgoals</p>



<a name="231810829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810829">(Mar 25 2021 at 14:30)</a>:</h4>
<p>and hence there is only one "minimum", the positive one</p>



<a name="231810842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810842">(Mar 25 2021 at 14:30)</a>:</h4>
<p>but anyway</p>



<a name="231810908"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810908" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810908">(Mar 25 2021 at 14:31)</a>:</h4>
<p>so, let's work through what would happen if we <em>just</em> updated the positive minimum for a coinductive goal</p>



<a name="231810951"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810951" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810951">(Mar 25 2021 at 14:31)</a>:</h4>
<p>(side note: it's so hard to figure out how to represent the stack etc)</p>



<a name="231810959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810959">(Mar 25 2021 at 14:31)</a>:</h4>
<p>that is, in the hackmd</p>



<a name="231810989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231810989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231810989">(Mar 25 2021 at 14:31)</a>:</h4>
<p>let me add a few more details</p>



<a name="231811744"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811744" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811744">(Mar 25 2021 at 14:35)</a>:</h4>
<p>ok so I expanded it a bit</p>



<a name="231811761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811761">(Mar 25 2021 at 14:35)</a>:</h4>
<p>the <code>goal:</code> cases basically constitute the <em>stack</em></p>



<a name="231811831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811831">(Mar 25 2021 at 14:35)</a>:</h4>
<p>and I just labeled the stack depth</p>



<a name="231811842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811842">(Mar 25 2021 at 14:36)</a>:</h4>
<p>so the minimum here would be depth 1</p>



<a name="231811947"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811947" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811947">(Mar 25 2021 at 14:36)</a>:</h4>
<p>in that case, we would consider <code>!X: C1</code> to be "ok" but we would return a minimum of 1</p>



<a name="231811979"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231811979" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231811979">(Mar 25 2021 at 14:36)</a>:</h4>
<p>this would mean that we would not cache the result</p>



<a name="231812020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812020">(Mar 25 2021 at 14:37)</a>:</h4>
<p>actually wait, where was that cycle detected again...</p>



<a name="231812084"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812084" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812084">(Mar 25 2021 at 14:37)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/a0eac73f60ad0ab1de2075def346bd5a5f2352cd/chalk-recursive/src/recursive.rs#L231-L241">here</a></p>



<a name="231812107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812107">(Mar 25 2021 at 14:37)</a>:</h4>
<p>so actually we never cached the <code>!X: C1</code> result</p>



<a name="231812126"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812126" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812126">(Mar 25 2021 at 14:37)</a>:</h4>
<p>it's the <code>X: C2</code> result that we cached, duh, but that also would not be cached here</p>



<a name="231812244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812244">(Mar 25 2021 at 14:38)</a>:</h4>
<p>ok, let's work through the other example</p>



<a name="231812287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812287">(Mar 25 2021 at 14:38)</a>:</h4>
<p><span class="user-mention silent" data-user-id="365822">FireFighterDuck</span> <a href="#narrow/stream/144729-wg-traits/topic/coinduction/near/230103152">said</a>:</p>
<blockquote>
<p>the <code>coinductive_unsound_inter_cycle_dependency</code> test I added in <a href="https://github.com/rust-lang/chalk/issues/690">chalk#690</a> .</p>
</blockquote>
<p>this one</p>



<a name="231812339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812339">(Mar 25 2021 at 14:39)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/3df6b429cbd801c5b4bf4b4ecc30732f59cba07a/tests/test/coinduction.rs#L433-L501">link</a></p>



<a name="231812377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812377">(Mar 25 2021 at 14:39)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="sd">/// Another test with two nested coinductive cycles.</span>
<span class="sd">/// Here the inner cycle is also dependent on the outer one.</span>
<span class="cp">#[test]</span><span class="w"></span>
<span class="k">fn</span> <span class="nf">coinductive_unsound_inter_cycle_dependency</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">test</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="n">program</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1andC2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C1</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C2</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C3</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C4</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C5</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C6</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="cp">#[coinductive]</span><span class="w"></span>
<span class="w">            </span><span class="k">trait</span><span class="w"> </span><span class="n">C7</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C5</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C6</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C7</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C5</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>:<span class="nc">C6</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C4</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C5</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C4</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C3</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>

<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">T</span>: <span class="nc">C1andC2</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C1</span><span class="p">,</span><span class="w"> </span><span class="n">T</span>: <span class="nc">C2</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>

<span class="w">        </span><span class="n">goal</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">forall</span><span class="o">&lt;</span><span class="n">X</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">X</span>: <span class="nc">C1andC2</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"> </span><span class="n">yields</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="s">"No possible solution"</span><span class="w"></span>
<span class="w">        </span><span class="p">}</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="231812384"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812384" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812384">(Mar 25 2021 at 14:39)</a>:</h4>
<p>good lord :)</p>



<a name="231812393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812393">(Mar 25 2021 at 14:39)</a>:</h4>
<p>let me condense that down</p>



<a name="231812466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812466">(Mar 25 2021 at 14:39)</a>:</h4>
<p>oh goodness</p>



<a name="231812565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812565">(Mar 25 2021 at 14:40)</a>:</h4>
<div class="codehilite"><pre><span></span><code>C1andC2 :- C1, C2.
C1 :- C3.
C2 :- C5, C1.
C3 :- C4.
C3 :- C5.
C4 :- C1.
C5 :- C6.
C6 :- C2, C7.
</code></pre></div>



<a name="231812609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812609">(Mar 25 2021 at 14:40)</a>:</h4>
<p>so what happens here...</p>



<a name="231812628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812628">(Mar 25 2021 at 14:40)</a>:</h4>
<p>I also made that one (more or less iirc) into a graph that may be easier to read <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span> <a href="https://github.com/rust-lang/chalk/blob/3df6b429cbd801c5b4bf4b4ecc30732f59cba07a/book/src/recursive/coinduction.md">https://github.com/rust-lang/chalk/blob/3df6b429cbd801c5b4bf4b4ecc30732f59cba07a/book/src/recursive/coinduction.md</a></p>



<a name="231812716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812716">(Mar 25 2021 at 14:41)</a>:</h4>
<p>ah, nice</p>



<a name="231812723"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812723" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812723">(Mar 25 2021 at 14:41)</a>:</h4>
<p>too bad github doesn't know how to render that</p>



<a name="231812756"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812756" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812756">(Mar 25 2021 at 14:41)</a>:</h4>
<p>but there's a mermaid live editor</p>



<a name="231812856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812856">(Mar 25 2021 at 14:41)</a>:</h4>
<p><a href="https://mermaid-js.github.io/mermaid-live-editor/#/edit/eyJjb2RlIjoiZ3JhcGggVERcbiAgQy0tPkMxO1xuICBDMS0tPkMzO1xuICBDMy0uLT5DNTtcbiAgQzMtLi0-QzQ7XG4gIEM0LS0-QzE7XG4gIEM1LS0-QzY7XG4gIEMtLT5DMjtcbiAgQzItLT5DNTtcbiAgQzItLT5DMTtcbiAgQzYtLT5DNztcbiAgQzYtLT5DMjsiLCJtZXJtYWlkIjp7InRoZW1lIjoiZGVmYXVsdCJ9LCJ1cGRhdGVFZGl0b3IiOmZhbHNlfQ">https://mermaid-js.github.io/mermaid-live-editor/#/edit/eyJjb2RlIjoiZ3JhcGggVERcbiAgQy0tPkMxO1xuICBDMS0tPkMzO1xuICBDMy0uLT5DNTtcbiAgQzMtLi0-QzQ7XG4gIEM0LS0-QzE7XG4gIEM1LS0-QzY7XG4gIEMtLT5DMjtcbiAgQzItLT5DNTtcbiAgQzItLT5DMTtcbiAgQzYtLT5DNztcbiAgQzYtLT5DMjsiLCJtZXJtYWlkIjp7InRoZW1lIjoiZGVmYXVsdCJ9LCJ1cGRhdGVFZGl0b3IiOmZhbHNlfQ</a></p>



<a name="231812970"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231812970" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231812970">(Mar 25 2021 at 14:42)</a>:</h4>
<p>that's beautiful</p>



<a name="231813000"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813000" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813000">(Mar 25 2021 at 14:42)</a>:</h4>
<p>dang, zulip is not embedding it =)</p>



<a name="231813172"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813172" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813172">(Mar 25 2021 at 14:43)</a>:</h4>
<p>ok so the "inner cycle" here is C5, C6, C2</p>



<a name="231813331"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813331" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813331">(Mar 25 2021 at 14:44)</a>:</h4>
<p>this is ultimately not provable because C6 is false</p>



<a name="231813343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813343">(Mar 25 2021 at 14:44)</a>:</h4>
<p>or rather C7 is false</p>



<a name="231813436"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813436" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813436">(Mar 25 2021 at 14:44)</a>:</h4>
<p>C1 is provable, though, right? because C1, C3, C4</p>



<a name="231813613"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813613" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813613">(Mar 25 2021 at 14:45)</a>:</h4>
<p>seems so</p>



<a name="231813869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813869">(Mar 25 2021 at 14:46)</a>:</h4>
<p>we didn't really cover the whole caching mechanism in detail</p>



<a name="231813898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813898">(Mar 25 2021 at 14:47)</a>:</h4>
<p>the current setup is that we have a <em>search graph</em> and a <em>stack</em></p>



<a name="231813926"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813926" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813926">(Mar 25 2021 at 14:47)</a>:</h4>
<p>this is entangled, side note, with my plans to make chalk more parallelizable</p>



<a name="231813947"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813947" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813947">(Mar 25 2021 at 14:47)</a>:</h4>
<p>there is also a cache</p>



<a name="231813971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813971">(Mar 25 2021 at 14:47)</a>:</h4>
<p>I think the search graph and stack should be thread-local</p>



<a name="231813980"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813980" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813980">(Mar 25 2021 at 14:47)</a>:</h4>
<p>but the cache should be shared</p>



<a name="231813986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231813986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231813986">(Mar 25 2021 at 14:47)</a>:</h4>
<p>right now they are all kind of shared</p>



<a name="231814057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814057">(Mar 25 2021 at 14:47)</a>:</h4>
<p>the search graph contains things tracked by their <em>depth first search number</em></p>



<a name="231814117"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814117" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814117">(Mar 25 2021 at 14:48)</a>:</h4>
<p>which is distinct from the stack depth, monotonically increasing</p>



<a name="231814269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814269">(Mar 25 2021 at 14:49)</a>:</h4>
<p>let me expand the previous example a bit just to bring it fresh in mind</p>



<a name="231814385"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814385" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814385">(Mar 25 2021 at 14:49)</a>:</h4>
<p>(actually the dfn maybe doesn't monotonically increase when we do caching, I forget, but anyway in this case it will)</p>



<a name="231814481"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814481" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814481">(Mar 25 2021 at 14:50)</a>:</h4>
<p>so basically when we finish proving <code>X: C2</code> we have a minimum of 1 so we leave the goal in the graph</p>



<a name="231814573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814573">(Mar 25 2021 at 14:50)</a>:</h4>
<p>(instead of moving it to the cache)</p>



<a name="231814589"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814589" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814589">(Mar 25 2021 at 14:50)</a>:</h4>
<p>then we compute the next goal: <code>!X: C3</code></p>



<a name="231814659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814659">(Mar 25 2021 at 14:51)</a>:</h4>
<p>this fails, minimum is INT_MAX (no cycle)</p>



<a name="231814676"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814676" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814676">(Mar 25 2021 at 14:51)</a>:</h4>
<p>but when we combine those the minimum remains 1</p>



<a name="231814787"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814787" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814787">(Mar 25 2021 at 14:51)</a>:</h4>
<p>so I think the bug that <span class="user-mention" data-user-id="365822">@FireFighterDuck</span> was pointing out is that now the goal at depth 1 has a minimum of 1, so once we reach a fixed point, we imagine that we can move things into the cache, but actually there are some incorrect results in the graph</p>



<a name="231814858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814858">(Mar 25 2021 at 14:52)</a>:</h4>
<p>in particular, we still have a recorded result of <code>Ok()</code> for <code>C2</code></p>



<a name="231814872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814872">(Mar 25 2021 at 14:52)</a>:</h4>
<p>(is that correct, <span class="user-mention" data-user-id="365822">@FireFighterDuck</span> ?)</p>



<a name="231814927"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814927" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814927">(Mar 25 2021 at 14:52)</a>:</h4>
<p>(this was not the full proposal that I proposed in the issue; only a piece of it)</p>



<a name="231814964"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231814964" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231814964">(Mar 25 2021 at 14:52)</a>:</h4>
<p>the problem here is that we didn't really do the 'fixed point' thing correctly</p>



<a name="231815081"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815081" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815081">(Mar 25 2021 at 14:53)</a>:</h4>
<p>in particular, the solution I was proposing in the issue would have worked somewhat differently</p>



<a name="231815163"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815163" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815163">(Mar 25 2021 at 14:53)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016">this solution</a></p>



<a name="231815289"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815289" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815289">(Mar 25 2021 at 14:54)</a>:</h4>
<p>let's give it a better name</p>



<a name="231815322"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815322" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815322">(Mar 25 2021 at 14:54)</a>:</h4>
<p>I'm just going to call it Solution0 :)</p>



<a name="231815447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815447">(Mar 25 2021 at 14:55)</a>:</h4>
<p>if we had used Solution0 in full, we would have started the goal at depth 1 with a result of <code>Ok</code></p>



<a name="231815541"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815541" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815541">(Mar 25 2021 at 14:55)</a>:</h4>
<p>when we encounter a cycle, we wouldn't special coinduction except in one way</p>



<a name="231815585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815585">(Mar 25 2021 at 14:55)</a>:</h4>
<p>we would detect a "mixed cycle" where the head is coinductive but there are inductive goals on the stack and force that to Err</p>



<a name="231815607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815607">(Mar 25 2021 at 14:55)</a>:</h4>
<p>(I think?)</p>



<a name="231815665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815665">(Mar 25 2021 at 14:56)</a>:</h4>
<p>/me thinks</p>



<a name="231815722"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815722" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815722">(Mar 25 2021 at 14:56)</a>:</h4>
<p>ok I have to think about that but never mind</p>



<a name="231815803"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815803" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815803">(Mar 25 2021 at 14:56)</a>:</h4>
<p>point is, we would update the minimums in the same way, but when we got back to the loop around <code>!X: C1</code></p>



<a name="231815829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815829">(Mar 25 2021 at 14:57)</a>:</h4>
<p>we would change the result from <code>Ok()</code> to <code>Err</code></p>



<a name="231815835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815835">(Mar 25 2021 at 14:57)</a>:</h4>
<p>and repeat the loop</p>



<a name="231815872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815872">(Mar 25 2021 at 14:57)</a>:</h4>
<p>this time when we get to <code>!X: C2 :- !X: C1</code> we would get back an <em>error</em></p>



<a name="231815887"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815887" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815887">(Mar 25 2021 at 14:57)</a>:</h4>
<p>(even though it's a coinductive cycle)</p>



<a name="231815950"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815950" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815950">(Mar 25 2021 at 14:57)</a>:</h4>
<p>and so the final result would be that <code>!X: C2</code> cannot be proven</p>



<a name="231815961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231815961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231815961">(Mar 25 2021 at 14:57)</a>:</h4>
<p>which I believe is correct</p>



<a name="231816285"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816285" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816285">(Mar 25 2021 at 14:59)</a>:</h4>
<p>I elaborated this in the hackmd</p>



<a name="231816300"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816300" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816300">(Mar 25 2021 at 14:59)</a>:</h4>
<p><a href="https://hackmd.io/2nm3xPJ1TTGc2r4iiWi4Lg?view#Solution0">here</a></p>



<a name="231816361"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816361" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816361">(Mar 25 2021 at 14:59)</a>:</h4>
<p>does that sound right so far?</p>



<a name="231816373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816373">(Mar 25 2021 at 14:59)</a>:</h4>
<p>(I want to look at the inner cycle test next)</p>



<a name="231816403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816403">(Mar 25 2021 at 15:00)</a>:</h4>
<p>(and I have to come back to what to do with mixed cycles, but I believe the answer is error)</p>



<a name="231816491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816491">(Mar 25 2021 at 15:00)</a>:</h4>
<p>unfortunately I have another meeting now :)</p>



<a name="231816544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816544">(Mar 25 2021 at 15:00)</a>:</h4>
<p>I have 9-10 blocked out tomorrow again though</p>



<a name="231816563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816563">(Mar 25 2021 at 15:00)</a>:</h4>
<p>and maybe I'll pop back in later</p>



<a name="231816750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816750">(Mar 25 2021 at 15:01)</a>:</h4>
<p>I'll be here tomorrow too</p>



<a name="231816779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231816779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231816779">(Mar 25 2021 at 15:01)</a>:</h4>
<p>But maybe we want to discuss binder refactor PR too</p>



<a name="231894470"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231894470" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231894470">(Mar 25 2021 at 23:57)</a>:</h4>
<p>I don't usually work in this area so forgive my ignorance, but looking at the <code>C1andC2</code> example and solving it by hand, it seems that the easiest way is to reason about the negative graph. <code>C7</code> is unprovable, but it is a requirement for <code>C6</code> so that is not provable, so <code>C5</code> is not provable, so <code>C2</code> is not provable, so <code>C1andC2</code> is not provable. At that point we saturate; thus everything that remains - <code>C1</code>,<code>C3</code>,<code>C4</code> - is provable. This is just exploiting that the negation of a coinductive predicate is inductive, so we can get at it with a simple connectivity search (working backward along edges, with "and" and "or" flipped).</p>



<a name="231903364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231903364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231903364">(Mar 26 2021 at 01:52)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> so there's a few problems with that approach. I think first is that even we do have a "tree", it's not clear where the "leaves" are. Let's say you <em>didn't</em> have <code>C7</code>, where would you start to "work backward"? Or, imagine that these clauses had conditions for them to be true? You essentially start to have a totally different problem of "where do I start". Also, if you start with what you <em>need</em> and go through all the ways that <em>could</em> be true, you do theoretically the minimal work to solve the goal. (You could imagine multiple separate trees too; if you wanted to solve a goal, you would on average need to go through several trees before getting to the one you need)</p>



<a name="231903480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/231903480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#231903480">(Mar 26 2021 at 01:55)</a>:</h4>
<p>That's not to say it isn't possible :) I'm by no means an expert in prolog solvers (barely a beginner in the grand scheme of things). So it would be interesting if there's any work on that sort of approach</p>



<a name="232009375"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232009375" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232009375">(Mar 26 2021 at 18:08)</a>:</h4>
<p>Right, I think you have to combine the work of discovering the tree with pruning leaves that are proven impossible. It's probably not too far from what you are doing already but maybe it helps conceptualize it better</p>



<a name="232011982"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232011982" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232011982">(Mar 26 2021 at 18:29)</a>:</h4>
<p>So during solving you get three states: true, false, and "maybe" or "not yet refuted". A maybe node becomes false if one of its dependencies becomes false. So this ends up looking like a DFS interspersed with a refutation:</p>
<ul>
<li>frontier = <code>C1andC2</code>, expand <code>C1andC2</code></li>
<li><code>C1andC2</code>: maybe, frontier = <code>C1, C2</code>, expand <code>C1</code></li>
<li><code>C1andC2, C1, C2</code>: maybe, frontier = <code>C3, C2</code>, expand <code>C3</code></li>
<li><code>C1andC2, C1, C2, C3</code>: maybe, frontier = <code>C4, C5, C2</code>, expand <code>C4</code></li>
<li><code>C1andC2, C1, C2, C3, C4</code>: maybe, frontier = <code>C5, C2</code>, expand <code>C5</code></li>
<li><code>C1andC2, C1, C2, C3, C4, C5</code>: maybe, frontier = <code>C6, C2</code>, expand <code>C6</code></li>
<li><code>C1andC2, C1, C2, C3, C4, C5, C6</code>: maybe, frontier = <code>C2, C7</code>, expand <code>C2</code></li>
<li><code>C1andC2, C1, C2, C3, C4, C5, C6</code>: maybe, frontier = <code>C7</code>, expand <code>C7</code></li>
<li><code>C1andC2, C1, C2, C3, C4, C5, C6</code>: maybe, <code>C7</code>: false, frontier = empty, refute <code>C7</code></li>
<li><code>C1andC2, C1, C2, C3, C4, C5</code>: maybe, <code>C6, C7</code>: false, frontier = empty, refute <code>C6</code></li>
<li><code>C1andC2, C1, C2, C3, C4</code>: maybe, <code>C5, C6, C7</code>: false, frontier = empty, refute <code>C5</code></li>
<li><code>C1andC2, C1, C3, C4</code>: maybe, <code>C2, C5, C6, C7</code>: false, frontier = empty, refute <code>C2</code></li>
<li><code>C1, C3, C4</code>: maybe, <code>C1andC2, C2, C5, C6, C7</code>: false, frontier = empty, refute <code>C1andC2</code></li>
</ul>
<p>This is the last step since we only care to refute the original goal <code>C1andC2</code>, but if we wanted to prove <code>C1</code> we would continue for one more step, see that nothing remains to be refuted, and conclude that all the maybes are true.</p>



<a name="232012874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232012874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232012874">(Mar 26 2021 at 18:35)</a>:</h4>
<p>If there are an infinite number of nodes and the graph is lazily expanded, this approach can be incomplete, for example if <code>Cn :- C(n+1)</code> then we would like to conclude that <code>C0</code> is true (coinductively) but it's hard to discover this unless you can see the whole graph</p>



<a name="232024925"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232024925" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232024925">(Mar 26 2021 at 20:09)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span>  Your description is actually pretty similar to how the recursive solver works. There are a few differences though. On one hand, Chalk needs to compute not only true and false but type constraints as well.  Thus, a true solution can also be ambiguous with some restraints (e.g. all types that implement <code>Size</code>). On the other hand, your deduction would most likely not refute C1andC2 directly when it hasn't even finished C1 (at least if it works the same way Chalk is currently implemented). This kind of connection is - as far as I understand - not feasible to check in the midst of another computation. I'm not quite sure whether the SLG solver could do this. <span class="user-mention" data-user-id="232957">@Jack Huey</span> could probably tell you more about this. <br>
On another note, do you already know the <a href="https://rust-lang.github.io/chalk/book/what_is_chalk.html">Chalk book</a>? It's a really good introduction to Chalk and the quite fascinating theory behind its two solvers :D</p>



<a name="232025887"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232025887" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232025887">(Mar 26 2021 at 20:16)</a>:</h4>
<p>I don't really have time right now to read through this and comment right, but if I remember, I'll get to it later :)</p>



<a name="232264611"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264611" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264611">(Mar 29 2021 at 13:08)</a>:</h4>
<p>I thought we could talk about this today</p>



<a name="232264624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264624">(Mar 29 2021 at 13:08)</a>:</h4>
<p>At least for a bit :)</p>



<a name="232264645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264645">(Mar 29 2021 at 13:08)</a>:</h4>
<p>I have to bring back the context in my head though</p>



<a name="232264669"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264669" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264669">(Mar 29 2021 at 13:08)</a>:</h4>
<p>I've also got to grind some coffee beans <span aria-label="coffee" class="emoji emoji-2615" role="img" title="coffee">:coffee:</span></p>



<a name="232264694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264694">(Mar 29 2021 at 13:08)</a>:</h4>
<p>I like how <code>:coff</code> brings up <span aria-label="coffin" class="emoji emoji-26b0" role="img" title="coffin">:coffin:</span> too</p>



<a name="232264796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264796">(Mar 29 2021 at 13:09)</a>:</h4>
<p>are emoticons suggesting something to coffee lovers?</p>



<a name="232264821"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264821" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264821">(Mar 29 2021 at 13:09)</a>:</h4>
<div class="message_inline_image"><a href="https://i.pinimg.com/originals/e3/c9/b0/e3c9b0a8d07b34357a2089f66018c486.jpg"><img src="https://i.pinimg.com/originals/e3/c9/b0/e3c9b0a8d07b34357a2089f66018c486.jpg"></a></div>



<a name="232264850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232264850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232264850">(Mar 29 2021 at 13:09)</a>:</h4>
<p>lol</p>



<a name="232265124"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265124" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265124">(Mar 29 2021 at 13:11)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/coinduction/near/231815722">said</a>:</p>
<blockquote>
<p>ok I have to think about that but never mind</p>
</blockquote>
<p>I have to re-read from this point</p>



<a name="232265137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265137">(Mar 29 2021 at 13:11)</a>:</h4>
<p>not sure who's around :)</p>



<a name="232265372"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265372" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265372">(Mar 29 2021 at 13:13)</a>:</h4>
<p><span class="user-mention" data-user-id="116266">@Santiago Pastorino</span> have you followed any of this so far?</p>



<a name="232265384"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265384" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265384">(Mar 29 2021 at 13:13)</a>:</h4>
<p>nope :)</p>



<a name="232265420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265420">(Mar 29 2021 at 13:13)</a>:</h4>
<p>I was reading the book and thought ... well some point I'm going to read about coinduction so let's keep reading :)</p>



<a name="232265761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265761">(Mar 29 2021 at 13:16)</a>:</h4>
<p>heh</p>



<a name="232265783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265783">(Mar 29 2021 at 13:16)</a>:</h4>
<p>well let's put 15-20 minutes into it...</p>



<a name="232265852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265852">(Mar 29 2021 at 13:17)</a>:</h4>
<p>I had a hackmd</p>



<a name="232265884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232265884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232265884">(Mar 29 2021 at 13:17)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/144729-wg-traits/topic/coinduction/near/231805718">said</a>:</p>
<blockquote>
<p><a href="https://hackmd.io/2nm3xPJ1TTGc2r4iiWi4Lg">https://hackmd.io/2nm3xPJ1TTGc2r4iiWi4Lg</a></p>
</blockquote>
<p>ah here it is</p>



<a name="232266116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266116">(Mar 29 2021 at 13:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116266">@Santiago Pastorino</span> the <em>basic</em> idea is that 'cycles are ok'</p>



<a name="232266161"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266161" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266161">(Mar 29 2021 at 13:19)</a>:</h4>
<p>so e.g. you can have cyclic rules like "<code>Foo</code> is true if <code>Foo</code> is true"</p>



<a name="232266166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266166">(Mar 29 2021 at 13:19)</a>:</h4>
<p><code>Foo :- Foo</code></p>



<a name="232266184"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266184" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266184">(Mar 29 2021 at 13:19)</a>:</h4>
<p>this comes up with proving autotraits like <code>Send</code></p>



<a name="232266188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266188">(Mar 29 2021 at 13:20)</a>:</h4>
<p>because you might e.g. have</p>



<a name="232266253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266253">(Mar 29 2021 at 13:20)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">struct</span> <span class="nc">List</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">data</span>: <span class="nc">T</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="n">next</span><span class="w"> </span>: <span class="nb">Option</span><span class="o">&lt;</span><span class="nb">Box</span><span class="o">&lt;</span><span class="n">List</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;&gt;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="232266263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266263">(Mar 29 2021 at 13:20)</a>:</h4>
<p>and this might give rise to a rule like</p>



<a name="232266306"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266306" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266306">(Mar 29 2021 at 13:20)</a>:</h4>
<div class="codehilite"><pre><span></span><code>Implemented(List&lt;T&gt;: Send) :-
    Implemented(T: Send),
    Implemented(Option&lt;Box&lt;List&lt;T&gt;&gt;&gt;: Send).
</code></pre></div>



<a name="232266353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266353">(Mar 29 2021 at 13:21)</a>:</h4>
<p>if you trace this out, you'll find that to prove that <code>Option&lt;Box&lt;List&lt;T&gt;&gt;&gt;: Send</code> you ultimately have to prove <code>List&lt;T&gt;: Send</code>, which is what you were trying to prove in the first place</p>



<a name="232266361"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266361" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266361">(Mar 29 2021 at 13:21)</a>:</h4>
<p><em>and that's ok</em></p>



<a name="232266739"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266739" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266739">(Mar 29 2021 at 13:23)</a>:</h4>
<p>anyway I think what I wanted to do was to work through this nested cycle example</p>



<a name="232266934"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266934" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266934">(Mar 29 2021 at 13:25)</a>:</h4>
<p>ohh I see</p>



<a name="232266939"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232266939" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232266939">(Mar 29 2021 at 13:25)</a>:</h4>
<p><span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span></p>



<a name="232267283"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267283" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267283">(Mar 29 2021 at 13:27)</a>:</h4>
<p>ok so the inner cycle test</p>



<a name="232267296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267296">(Mar 29 2021 at 13:27)</a>:</h4>
<div class="codehilite"><pre><span></span><code>C1andC2 :- C1, C2.
C1 :- C3.
C2 :- C5, C1.
C3 :- C4.
C3 :- C5.
C4 :- C1.
C5 :- C6.
C6 :- C2, C7.
</code></pre></div>



<a name="232267342"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267342" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267342">(Mar 29 2021 at 13:28)</a>:</h4>
<p>let's walk through it, using Solution0</p>



<a name="232267386"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267386" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267386">(Mar 29 2021 at 13:28)</a>:</h4>
<p>to start, we have the goal <code>C1andC2</code></p>



<a name="232267746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267746">(Mar 29 2021 at 13:30)</a>:</h4>
<div class="codehilite"><pre><span></span><code>* clause: `C1andC2 :- C1, C2`
</code></pre></div>



<a name="232267765"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267765" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267765">(Mar 29 2021 at 13:30)</a>:</h4>
<p>you're talking about the example from the HackMD?</p>



<a name="232267776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267776">(Mar 29 2021 at 13:30)</a>:</h4>
<p>yeah</p>



<a name="232267796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267796">(Mar 29 2021 at 13:31)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/3df6b429cbd801c5b4bf4b4ecc30732f59cba07a/tests/test/coinduction.rs#L433-L501">link</a></p>



<a name="232267797"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232267797" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232267797">(Mar 29 2021 at 13:31)</a>:</h4>
<p>ahh the last one</p>



<a name="232268614"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232268614" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232268614">(Mar 29 2021 at 13:36)</a>:</h4>
<p>ps, <span class="user-mention" data-user-id="271719">@Mario Carneiro</span> I didn't forget about you, I just want to work through this example before I circle back and read what you're saying in depth :)</p>



<a name="232269882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232269882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232269882">(Mar 29 2021 at 13:44)</a>:</h4>
<p>no worries, I'm not speaking with respect to the current algorithm in chalk so it probably isn't immediately useful</p>



<a name="232271045"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271045" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271045">(Mar 29 2021 at 13:51)</a>:</h4>
<p>ok, I worked through the example</p>



<a name="232271076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271076">(Mar 29 2021 at 13:51)</a>:</h4>
<p>as far as I can tell, Solution0 handles the nested cycle case correctly</p>



<a name="232271081"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271081" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271081">(Mar 29 2021 at 13:51)</a>:</h4>
<p><span class="user-mention" data-user-id="365822">@FireFighterDuck</span> do you happen to be around?</p>



<a name="232271233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271233">(Mar 29 2021 at 13:52)</a>:</h4>
<p>so-- I'm thinking about your PR :)</p>



<a name="232271256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271256">(Mar 29 2021 at 13:52)</a>:</h4>
<p>I think there's an easier way to do it</p>



<a name="232271346"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271346" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271346">(Mar 29 2021 at 13:53)</a>:</h4>
<p>but to start, do these results look correct to you for the nested cycle example?</p>



<a name="232271354"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271354" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271354">(Mar 29 2021 at 13:53)</a>:</h4>
<p>Final cache:</p>
<ul>
<li><code>C1 =&gt; Ok</code></li>
<li><code>C2 =&gt; error</code></li>
<li><code>C3 =&gt; Ok</code></li>
<li><code>C4 =&gt; Ok</code></li>
<li><code>C5 =&gt; error</code></li>
<li><code>C6 =&gt; error</code></li>
<li><code>C7 =&gt; error</code></li>
<li><code>C1andC2 =&gt; Error</code></li>
</ul>



<a name="232271632"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271632" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271632">(Mar 29 2021 at 13:54)</a>:</h4>
<p>it looks right to me</p>



<a name="232271648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271648">(Mar 29 2021 at 13:54)</a>:</h4>
<p>Yes, these should be the correct results.</p>



<a name="232271700"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271700" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271700">(Mar 29 2021 at 13:55)</a>:</h4>
<p>so the important thing is to start the "initial value" for coinductive goals to <code>Ok</code> and to iterate if it changes</p>



<a name="232271738"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232271738" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232271738">(Mar 29 2021 at 13:55)</a>:</h4>
<p>(that said, I have to think about what to do with mixed cycles, I think the answer is that it is just always an error)</p>



<a name="232272262"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232272262" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232272262">(Mar 29 2021 at 13:59)</a>:</h4>
<p>Thanks to your explanation of Solution0, I finally understood how it should work. There were some minor misunderstandings on my part. Nonetheless, I would try to come up with an implementation of Solution0 in a new PR if that's okay for you.</p>



<a name="232272704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232272704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232272704">(Mar 29 2021 at 14:01)</a>:</h4>
<p>Agreed</p>



<a name="232272707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232272707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232272707">(Mar 29 2021 at 14:01)</a>:</h4>
<p>Keep the old one :)</p>



<a name="232273044"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232273044" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232273044">(Mar 29 2021 at 14:03)</a>:</h4>
<p>sadly I have to run for now</p>



<a name="232342200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232342200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232342200">(Mar 29 2021 at 21:52)</a>:</h4>
<blockquote>
<p>I think the answer is that it is just always an error</p>
</blockquote>
<p>i would intuitively expect mixed cycles to be fine. This is really interesting to me, so in case you remember then, please ping me if you make progress here <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span></p>



<a name="232766445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232766445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232766445">(Apr 01 2021 at 14:33)</a>:</h4>
<p><span class="user-mention" data-user-id="365822">@FireFighterDuck</span> just saw <a href="https://github.com/rust-lang/chalk/pull/698">https://github.com/rust-lang/chalk/pull/698</a></p>



<a name="232766449"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232766449" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232766449">(Apr 01 2021 at 14:33)</a>:</h4>
<p>that was fast!</p>



<a name="232767780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232767780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232767780">(Apr 01 2021 at 14:40)</a>:</h4>
<p>Fortunately, solution0 is pretty similar to my first approach. I hope I implemented solution0 correctly; it works at least for all tests and behaves exactly as described in the hackmd for the inner cycle example.</p>



<a name="232899989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction/near/232899989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.html#232899989">(Apr 02 2021 at 13:43)</a>:</h4>
<p>I'll do some reviewing</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>